\begin{tabbing}
usends1{-}p(${\it es}$;${\it ds}$;$k$;$T$;$l$;${\it tg}$;$B$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(($\forall$$x$:Id. subtype\_rel(es{-}vartype(${\it es}$; source($l$); $x$); fpf{-}cap(${\it ds}$; id{-}deq; $x$; top)))\+
\\[0ex]$\wedge$ alle{-}at(\=${\it es}$;\+
\\[0ex]source($l$);
\\[0ex]$e$.((es{-}kind(${\it es}$; $e$) = $k$ $\in$ Knd) $\Rightarrow$ subtype\_rel(es{-}valtype(${\it es}$; $e$); $T$)))
\-\\[0ex]$\wedge$ \=($\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex](es{-}kind(${\it es}$; $e$) = rcv($l$,${\it tg}$) $\in$ Knd) $\Rightarrow$ subtype\_rel(es{-}valtype(${\it es}$; $e$); $B$)))
\-\\[0ex]c$\wedge$ alle{-}at(\=${\it es}$;\+
\\[0ex]source($l$);
\\[0ex]$e$.((es{-}kind(${\it es}$; $e$) = $k$ $\in$ Knd)
\\[0ex]$\Rightarrow$ ($\exists$\=${\it e'}$:es{-}E(${\it es}$)\+
\\[0ex]((es{-}kind(${\it es}$; ${\it e'}$) = rcv($l$,${\it tg}$) $\in$ Knd)
\\[0ex]c$\wedge$ \=((es{-}sender(${\it es}$; ${\it e'}$) = $e$ $\in$ es{-}E(${\it es}$))\+
\\[0ex]$\wedge$ \=($\forall$${\it e''}$:es{-}E(${\it es}$). \+
\\[0ex](es{-}kind(${\it es}$; ${\it e''}$) = rcv($l$,${\it tg}$) $\in$ Knd)
\\[0ex]$\Rightarrow$ (es{-}sender(${\it es}$; ${\it e''}$) = $e$ $\in$ es{-}E(${\it es}$))
\\[0ex]$\Rightarrow$ (${\it e''}$ = ${\it e'}$ $\in$ es{-}E(${\it es}$)))
\-\\[0ex]$\wedge$ (es{-}val(${\it es}$; ${\it e'}$) = $f$(es{-}state{-}when(${\it es}$; $e$),es{-}val(${\it es}$; $e$)) $\in$ $B$)))))
\-\-\\[0ex])
\-\-
\end{tabbing}